basic
Inj(A;B;f) == a1, a2:A. (f(a1) = f(a2))  (a1 = a2) 

latex

---

clarification:

basic
Inj(A;B;f) == a1:A, a2:A. (f(a1) = f(a2)  B)  (a1 = a2  A) 

latex

Up	fun 1, fun 1
Wellformedness Lemmas	inject wf, inject wf
Definitions	x:A. B(x), P  Q, f(a), s = t
FDL editor aliases	inject